ds:x:Id fp Type, da:k:Knd fp Type, A:ecl-trans-tuple{i:l}(ds;da).
ecl-trans-a(A)
 (k:{k:Knd| (k  ecl-trans-ks(A)) }State(ds)Valtype(da;k)ecl-trans-type(A)) 

latex

Definitions	t  T, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-a(v), ecl-trans-type(A), ecl-trans-ks(v), ecl-trans-tuple{i:l}(ds;da), Id, x. t(x), x:A. B(x), a:A fp B(a), Knd, , (x  l), State(ds), Valtype(da;k),
Lemmas	ecl-trans-tuple wf, Knd wf, fpf wf, Id wf